from copy import copy

from cheqed.core.graph.node import Node
from cheqed.core.graph.traversal import preorder_edges

from cheqed.core.side import LEFT, RIGHT, BOTH
from cheqed.core.sequent import Sequent

from cheqed.core import term, formula, rewrite

def require_operator(operator, side, sequent):
    if sequent[side][0].operator != operator.operator:
        raise ValueError()

class Rule(object):
    pass

class Hypothesis(Rule):
    top_arity = 0
    bottom_arity = 1
    side = BOTH
    index = 0
    name = "Hypothesis"

    def __init__(self, sequent):
        self.sequent = sequent

    def up(self):
        return []

    def down(self):
        return [ self.sequent ]

class Conclusion(Rule):
    top_arity = 1
    bottom_arity = 0    
    side = BOTH
    index = 0
    name = "Conclusion"
    
    def __init__(self, sequent):
        self.sequent = sequent

    def up(self):
        return [ self.sequent ]

    def down(self):
        return []

applicable_rules = []
def applicable(func):
    applicable_rules.append(func)

class Axiom(Rule):
    top_arity = 0
    bottom_arity = 1
    side = BOTH
    index = 0
    name = "Axiom"
    
    def __init__(self, sequent):
        if not sequent.left[0] == sequent.right[0]:
            raise ValueError()

        self.sequent = sequent

    def __eq__(self, other):
        return self.__class__ == other.__class__ \
               and self.sequent == other.sequent

    def up(self, bottom):
        return []

    def down(self):
        return [ self.sequent ]

    @classmethod
    def apply(cls, sequent):
        try:
            return [ cls(sequent) ]
        except:
            return []
applicable(Axiom.apply)

class Negation(Rule):
    top_arity = 1
    bottom_arity = 1
    index = 0

    @property
    def name(self):
        return str(self.side).capitalize() + " Negation"
    
    def __init__(self, side):
        self.side = side

    def __eq__(self, other):
        return self.__class__ == other.__class__ \
               and self.side == other.side

    def up(self, bottom):
        require_operator(formula.Negation, self.side, bottom)

        res = Sequent()
        negative = bottom[self.side][0]
        res[self.side.opposite()] = [ negative.args[0] ] + bottom[self.side.opposite()]
        res[self.side] = bottom[self.side][1:]
        return [ res ]
        
    def down(self, top):
        res = Sequent()
        res[self.side.opposite()] = top[self.side.opposite()][1:]
        res[self.side] = [ formula.Negation(top[self.side.opposite()][0]) ] \
                         + top[self.side]
        return [ res ]

    @classmethod
    def apply(cls, sequent):
        def apply_side(side):
            try:
                rule = cls(side)
                rule.up(sequent)            
                return [ rule ]
            except:
                return []

        return apply_side(LEFT) + apply_side(RIGHT)
applicable(Negation.apply)

class LeftDisjunction(Rule):
    top_arity = 2
    bottom_arity = 1
    side = LEFT
    index = 0
    name = "Left Disjunction"

    def __eq__(self, other):
        return self.__class__ == other.__class__
        
    @staticmethod
    def up(bottom):
        require_operator(formula.Disjunction, LEFT, bottom)
        
        conjunct = bottom.left[0]
        left0 = [ conjunct.args[0] ] + bottom.left[1:]
        left1 = [ conjunct.args[1] ] + bottom.left[1:]

        return [ Sequent(left0, bottom.right),
                 Sequent(left1, bottom.right) ]

    @staticmethod
    def down(*top):
        left = [ formula.Disjunction(top[0].left[0], top[1].left[0]) ] \
               + top[0].left[1:]

        return [ Sequent(left, top[0].right) ]

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(LeftDisjunction.apply)

class RightDisjunction(Rule):
    top_arity = 1
    bottom_arity = 1
    side = RIGHT
    index = 0
    name = "Right Disjunction"

    def __eq__(self, other):
        return self.__class__ == other.__class__
    
    @staticmethod
    def up(bottom):
        require_operator(formula.Disjunction, RIGHT, bottom)        

        disjunct = bottom.right[0]
        right = [ disjunct.args[0], disjunct.args[1] ] + bottom.right[1:]

        return [ Sequent(bottom.left, right) ]

    @staticmethod
    def down(*top):
        top = top[0]
        right = [ formula.Disjunction(top.right[0], top.right[1]) ] \
                + top.right[2:]

        return [ Sequent(top.left, right) ]

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(RightDisjunction.apply)

class LeftUniversal(Rule):
    top_arity = 1
    bottom_arity = 1
    side = LEFT
    index = 0
    witness_class = term.Term
    name = "Left Universal"

    def __init__(self, bound, witness=None):
        self.bound = bound
        self.witness = witness

    def __eq__(self, other):
        return self.__class__ == other.__class__ \
               and self.bound == other.bound \
               and self.witness == other.witness
        
    def up(self, bottom):
        require_operator(formula.Universal, LEFT, bottom)

        quantifier = bottom.left[0]
        quantified = quantifier.formula.substitute(self.witness, self.bound)
        left = [ quantified ] + bottom.left[1:]
        return [ Sequent(left, bottom.right) ]

    def down(self, top):
        quantified = top.left[0].substitute(self.bound, self.witness)
        left = [ formula.Universal(self.bound, quantified) ] \
               + top.left[1:]
        return [ Sequent(left, top.right) ]

    @classmethod
    def apply(cls, sequent):
        try:
            require_operator(formula.Universal, LEFT, sequent)
            return [ cls(sequent[LEFT][0].bound) ]
        except:
            return []
applicable(LeftUniversal.apply)

class RightUniversal(Rule):
    top_arity = 1
    bottom_arity = 1
    side = RIGHT
    index = 0
    witness_class = term.Variable
    name = "Right Universal"

    def __init__(self, bound, witness=None):
        self.bound = bound
        self.witness = witness

    def __eq__(self, other):
        return self.__class__ == other.__class__ \
               and self.bound == other.bound \
               and self.witness == other.witness
        
    def up(self, bottom):
        require_operator(formula.Universal, RIGHT, bottom)
        if self.witness in bottom.free_variables():
            raise ValueError()

        quantifier = bottom.right[0]
        quantified = quantifier.formula.substitute(self.witness, self.bound)
        right = [ quantified ] + bottom.right[1:]
        return [ Sequent(bottom.left, right) ]

    def down(self, top):
        quantified = top.right[0].substitute(self.bound, self.witness)
        right = [ formula.Universal(self.bound, quantified) ] + top.right[1:]

        return [ Sequent(top.left, right) ]

    @classmethod
    def apply(cls, sequent):
        try:
            require_operator(formula.Universal, RIGHT, sequent)
            return [ cls(sequent[RIGHT][0].bound) ]
        except:
            return []
applicable(RightUniversal.apply)

class Permutation(Rule):
    top_arity = 1
    bottom_arity = 1

    @property
    def name(self):
        return str(self.side).capitalize() + " Permutation"

    def __init__(self, side, index):
        self.side = side
        self.index = index

    def __eq__(self, other):
        return self.__class__ == other.__class__ \
               and self.side == other.side \
               and self.index == other.index
    
    def up(self, bottom):
        res = copy(bottom)
        res[self.side] = [ bottom[self.side][self.index] ] \
                         + bottom[self.side][:self.index] \
                         + bottom[self.side][self.index + 1:]
        return [ res ]

    def down(self, top):
        res = copy(top)
        res[self.side] = top[self.side][1:self.index + 1] \
                         + [ top[self.side][0] ] \
                         + top[self.side][self.index + 1:]
        return [ res ]

    @classmethod
    def apply(cls, sequent):
        def apply_side(side):
            return map(lambda index: cls(side, index),
                       range(len(sequent[side]))[1:])

        return apply_side(LEFT) + apply_side(RIGHT)
applicable(Permutation.apply)

class Weakening(Rule):
    top_arity = 1
    bottom_arity = 1

    @property
    def name(self):
        return str(self.side).capitalize() + " Weakening"

    def __init__(self, side, index, formula):
        self.side = side
        self.index = index
        self.formula = formula

    def __eq__(self, other):
        return self.__class__ == other.__class__ \
               and self.side == other.side \
               and self.index == other.index \
               and self.formula == other.formula
    
    def up(self, bottom):
        assert self.formula == bottom[self.side][self.index]
        res = copy(bottom)
        
        res[self.side] = (bottom[self.side][:self.index]
                          + bottom[self.side][self.index + 1:])
        return [ res ]

    def down(self, top):
        res = copy(top)
        res[self.side] = (top[self.side][:self.index]
                          + [ self.formula ]
                          + top[self.side][self.index:])
        return [ res ]

    @classmethod
    def apply(cls, sequent):
        def apply_side(side):
            return [ cls(side, index, formula)
                     for index, formula
                     in enumerate(sequent[side]) ]
        
        return apply_side(LEFT) + apply_side(RIGHT)
applicable(Weakening.apply)

class Contraction(Rule):
    top_arity = 1
    bottom_arity = 1

    @property
    def name(self):
        return str(self.side).capitalize() + " Contraction"

    def __init__(self, side, index):
        self.side = side
        self.index = index

    def __eq__(self, other):
        return (self.__class__ == other.__class__
                and self.side == other.side
                and self.index == other.index)
    
    def up(self, bottom):
        res = copy(bottom)
        
        res[self.side] = (bottom[self.side][:self.index]
                          + [ bottom[self.side][self.index] ]
                          + bottom[self.side][self.index:])
        return [ res ]

    def down(self, top):
        res = copy(top)
        res[self.side] = (top[self.side][:self.index]
                          + top[self.side][self.index + 1:])
        return [ res ]

    @classmethod
    def apply(cls, sequent):
        def apply_side(side):
            return [ cls(side, index)
                     for index, formula
                     in enumerate(sequent[side]) ]
        
        return apply_side(LEFT) + apply_side(RIGHT)
applicable(Contraction.apply)

class Abbreviation(Rule):
    top_arity = 1
    bottom_arity = 1
    index = 0

    @property
    def name(self):
        return str(self.side).capitalize() + " Abbreviation"
    
    def __init__(self, side):
        self.side = side

    def __eq__(self, other):
        return (self.__class__ == other.__class__
                and self.side == other.side)
    
    def up(self, bottom):
        try:
            exp = rewrite.expand(bottom[self.side][0])
        except rewrite.ExpansionError, err:
            raise ValueError(err.message)
        
        res = Sequent()
        res[self.side.opposite()] = bottom[self.side.opposite()]
        res[self.side] = [ exp ] + bottom[self.side][1:]
        return [ res ]

    def down(self, *top):
        top = top[0]
        res = Sequent()
        res[self.side.opposite()] = top[self.side.opposite()]
        res[self.side] = [ rewrite.simplify(top[self.side][0]) ] \
                         + top[self.side][1:]
        return [ res ]

    @classmethod
    def apply(cls, sequent):
        def apply_side(side):
            try:
                rule = cls(side)
                rule.up(sequent)            
                return [ rule ]
            except:
                return []

        return apply_side(LEFT) + apply_side(RIGHT)
applicable(Abbreviation.apply)

class DerivedRule(Rule):
    def __init__(self, make_proof, bottom_arity, top_arity, side, index):
        if make_proof is not None:
            self.make_proof = make_proof
        self.side = side
        self.index = index
        self.bottom_arity = bottom_arity
        self.top_arity = top_arity

    def __eq__(self, other):
        return (self.__class__ == other.__class__
                and self.make_proof == other.make_proof
                and self.index == other.index
                and self.side == other.side
                and self.bottom_arity == other.bottom_arity
                and self.top_arity == other.top_arity)
        
    def up(self, bottom):
        conclusion = Node(Conclusion(bottom))

        bottoms = [edge for edge in preorder_edges(self.make_proof().bottom)
                   if not edge.is_connected]

        assert len(bottoms) == 1
        conclusion.top[0].connect(bottoms[0])

        return [edge.sequent() for edge in preorder_edges(conclusion.top)
                if not edge.is_connected]

    def down(self, *top):
        proof = self.make_proof()
        tops = [edge for edge in preorder_edges(proof.top)
                if not edge.is_connected]
        assert len(top) == len(tops)
        
        for sequent, edge in zip(top, tops):
            edge.connect(Node(Hypothesis(sequent)).bottom[0])
            
        bottoms = [edge for edge in preorder_edges(proof.bottom)]
        assert len(bottoms) == 1

        return [ bottoms[0].sequent() ]

class RightExistential(DerivedRule):
    name = "Right Existential"
    witness_class = LeftUniversal.witness_class

    def make_proof(self):
        ab = Node(Abbreviation(RIGHT))
        rn = Node(Negation(RIGHT))
        lu = Node(LeftUniversal(self.bound, self.witness))
        ln = Node(Negation(LEFT))

        ab.top[0].connect(rn.bottom[0])
        rn.top[0].connect(lu.bottom[0])
        lu.top[0].connect(ln.bottom[0])

        return ab

    def __init__(self, bound, witness=None):
        self.bound = bound
        self.witness = witness
        DerivedRule.__init__(self, None, 1, 1, RIGHT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            require_operator(formula.Existential, RIGHT, sequent)
            return [ cls(sequent[RIGHT][0].bound) ]
        except:
            return []
applicable(RightExistential.apply)

class LeftExistential(DerivedRule):
    name = "Left Existential"
    witness_class = RightUniversal.witness_class

    def make_proof(self):
        ab = Node(Abbreviation(LEFT))
        ln = Node(Negation(LEFT))
        ru = Node(RightUniversal(self.bound, self.witness))
        rn = Node(Negation(RIGHT))

        ab.top[0].connect(ln.bottom[0])
        ln.top[0].connect(ru.bottom[0])
        ru.top[0].connect(rn.bottom[0])

        return ab

    def __init__(self, bound, witness=None):
        self.bound = bound
        self.witness = witness
        DerivedRule.__init__(self, None, 1, 1, LEFT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            require_operator(formula.Existential, LEFT, sequent)
            return [ cls(sequent[LEFT][0].bound) ]
        except:
            return []
applicable(LeftExistential.apply)

def right_conjunction_proof():
    ab = Node(Abbreviation(RIGHT))
    rn = Node(Negation(RIGHT))
    ld = Node(LeftDisjunction())
    ln0 = Node(Negation(LEFT))
    ln1 = Node(Negation(LEFT))

    ab.top[0].connect(rn.bottom[0])
    rn.top[0].connect(ld.bottom[0])
    ld.top[0].connect(ln0.bottom[0])
    ld.top[1].connect(ln1.bottom[0])

    return ab

class RightConjunction(DerivedRule):
    name = "Right Conjunction"

    def __init__(self):
        DerivedRule.__init__(self, right_conjunction_proof, 1, 2, RIGHT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(RightConjunction.apply)

def left_conjunction_proof():
    ab = Node(Abbreviation(LEFT))
    ln = Node(Negation(LEFT))
    rd = Node(RightDisjunction())
    rn0 = Node(Negation(RIGHT))
    rn1 = Node(Negation(RIGHT))

    ab.top[0].connect(ln.bottom[0])
    ln.top[0].connect(rd.bottom[0])
    rd.top[0].connect(rn0.bottom[0])
    rn0.top[0].connect(rn1.bottom[0])

    return ab

class LeftConjunction(DerivedRule):
    name = "Left Conjunction"

    def __init__(self):
        DerivedRule.__init__(self, left_conjunction_proof, 1, 1, LEFT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(LeftConjunction.apply)

def left_conditional_proof():
    ab = Node(Abbreviation(LEFT))
    ld = Node(LeftDisjunction())
    ln = Node(Negation(LEFT))

    ab.top[0].connect(ld.bottom[0])
    ld.top[0].connect(ln.bottom[0])

    return ab

class LeftConditional(DerivedRule):
    name = "Left Conditional"

    def __init__(self):
        DerivedRule.__init__(self, left_conditional_proof, 1, 2, LEFT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(LeftConditional.apply)

def right_conditional_proof():
    ab = Node(Abbreviation(RIGHT))
    rd = Node(RightDisjunction())
    rn = Node(Negation(RIGHT))

    ab.top[0].connect(rd.bottom[0])
    rd.top[0].connect(rn.bottom[0])

    return ab

class RightConditional(DerivedRule):
    name = "Right Conditional"

    def __init__(self):
        DerivedRule.__init__(self, right_conditional_proof, 1, 1, RIGHT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(RightConditional.apply)

def right_biconditional_proof():
    ab = Node(Abbreviation(RIGHT))
    rc = Node(RightConjunction())
    rc0 = Node(RightConditional())
    rc1 = Node(RightConditional())

    ab.top[0].connect(rc.bottom[0])
    rc.top[0].connect(rc0.bottom[0])
    rc.top[1].connect(rc1.bottom[0])

    return ab

class RightBiconditional(DerivedRule):
    name = "Right Biconditional"

    def __init__(self):
        DerivedRule.__init__(self, right_biconditional_proof, 1, 2, RIGHT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(RightBiconditional.apply)

def left_biconditional_proof():
    ab = Node(Abbreviation(LEFT))
    lc = Node(LeftConjunction())
    lc0 = Node(LeftConditional())
    lp = Node(Permutation(LEFT, 1))
    lc1 = Node(LeftConditional())
    lc2 = Node(LeftConditional())
    
    ab.top[0].connect(lc.bottom[0])
    lc.top[0].connect(lc0.bottom[0])
    lc0.top[1].connect(lp.bottom[0])
    lp.top[0].connect(lc1.bottom[0])
    lc0.top[0].connect(lc2.bottom[0])

    return ab

class LeftBiconditional(DerivedRule):
    name = "Left Biconditional"

    def __init__(self):
        DerivedRule.__init__(self, left_biconditional_proof, 1, 4, LEFT, 0)

    @classmethod
    def apply(cls, sequent):
        try:
            rule = cls()
            rule.up(sequent)
            return [ rule ]
        except:
            return []
applicable(LeftBiconditional.apply)
